not(and(x, y)) → or(not(x), not(y))
not(or(x, y)) → and(not(x), not(y))
and(x, or(y, z)) → or(and(x, y), and(x, z))
↳ QTRS
↳ DependencyPairsProof
not(and(x, y)) → or(not(x), not(y))
not(or(x, y)) → and(not(x), not(y))
and(x, or(y, z)) → or(and(x, y), and(x, z))
AND(x, or(y, z)) → AND(x, y)
NOT(and(x, y)) → NOT(y)
NOT(or(x, y)) → NOT(x)
NOT(and(x, y)) → NOT(x)
NOT(or(x, y)) → AND(not(x), not(y))
AND(x, or(y, z)) → AND(x, z)
NOT(or(x, y)) → NOT(y)
not(and(x, y)) → or(not(x), not(y))
not(or(x, y)) → and(not(x), not(y))
and(x, or(y, z)) → or(and(x, y), and(x, z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
AND(x, or(y, z)) → AND(x, y)
NOT(and(x, y)) → NOT(y)
NOT(or(x, y)) → NOT(x)
NOT(and(x, y)) → NOT(x)
NOT(or(x, y)) → AND(not(x), not(y))
AND(x, or(y, z)) → AND(x, z)
NOT(or(x, y)) → NOT(y)
not(and(x, y)) → or(not(x), not(y))
not(or(x, y)) → and(not(x), not(y))
and(x, or(y, z)) → or(and(x, y), and(x, z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
AND(x, or(y, z)) → AND(x, y)
AND(x, or(y, z)) → AND(x, z)
not(and(x, y)) → or(not(x), not(y))
not(or(x, y)) → and(not(x), not(y))
and(x, or(y, z)) → or(and(x, y), and(x, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
AND(x, or(y, z)) → AND(x, y)
AND(x, or(y, z)) → AND(x, z)
The value of delta used in the strict ordering is 4.
POL(AND(x1, x2)) = (4)x_2
POL(or(x1, x2)) = 1 + (4)x_1 + (4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
not(and(x, y)) → or(not(x), not(y))
not(or(x, y)) → and(not(x), not(y))
and(x, or(y, z)) → or(and(x, y), and(x, z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
NOT(and(x, y)) → NOT(y)
NOT(or(x, y)) → NOT(x)
NOT(and(x, y)) → NOT(x)
NOT(or(x, y)) → NOT(y)
not(and(x, y)) → or(not(x), not(y))
not(or(x, y)) → and(not(x), not(y))
and(x, or(y, z)) → or(and(x, y), and(x, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
NOT(and(x, y)) → NOT(y)
NOT(or(x, y)) → NOT(x)
NOT(and(x, y)) → NOT(x)
NOT(or(x, y)) → NOT(y)
The value of delta used in the strict ordering is 8.
POL(NOT(x1)) = (4)x_1
POL(or(x1, x2)) = 2 + (4)x_1 + (4)x_2
POL(and(x1, x2)) = 4 + (4)x_1 + (4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
not(and(x, y)) → or(not(x), not(y))
not(or(x, y)) → and(not(x), not(y))
and(x, or(y, z)) → or(and(x, y), and(x, z))